| Definitions |  x:A. B(x), sendMinimalR{$a:ut2, $tg:ut2}(T; t; l; ds1; ds2; P; Q; d1; d2; f), R-Feasible(R), P   Q, Normal(ds), State(ds),  , x:A  B(x),  b, x:A  B(x),  x:A. B(x), Dec(P),  , Type, a:A fp B(a), IdLnk, source(l), lnk-inv(l), Id, s = t,  A, x dom(f). v=f(x) P(x;v), False, rec(x.A(x)), DeclaredType(ds;x), Realizer, {x:A| B(x)} , a < b, t T, A  B,  , type List, Knd, left + right, FinProbSpace,   x. t(x),  , Unit, (x l), hd(l), i <z j, i z j, l[i], tl(l), weakSendDoApplyR{$a:ut2, $tg:ut2}(T; t; l; ds; f), [], [car / cdr], {T}, SQType(T),  , s ~ t, #$n, P  Q, ||as||, A c B, xL. P(x), {i..j }, f(a), A || B, True, P & Q,  b, P  Q, es realizer ind Rsframe compseq tag def, eq_atom$n(x;y), Atom2Deq, eqof(d), IdDeq, a = b, "$x", (i = j), Rsends-T(x1), Rsends-dt(x1), Rsends-l(x1), Rsends-knd(x1), Rsends?(x1), Reffect-T(x1), Reffect-knd(x1), Reffect?(x1), Rrframe-L(x1), Rpre-a(x1), Rpre-ds(x1), Rrframe-x(x1), Rrframe?(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-g(x1), Rsframe-tag(x1), Rsframe-lnk(x1), Rsframe?(x1), Reffect-ds(x1), Raframe-L(x1), Reffect-x(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Rframe-x(x1), Rframe?(x1), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), R-interface-compat(A;B), R-frame-compat(A;B), p = q, R-base-domain(R), Rda(R), Rds(R), R-loc(R), inr x , Rsframe(lnk;tag;L), Void,  x:A.B(x), Top, Rnone(), left  right, es realizer ind Rsends compseq tag def, Rsends(ds;knd;T;l;dt;g), Outcome, x : v, <a, b>, es realizer ind Rpre compseq tag def, Rpre(loc;ds;a;p;P), Atom$n, f(x)?z, *1*, i j < k, if b then t else f fi , mu'(P), do-apply(f;x), S  T, suptype(S; T), P Q,  T, x.A(x), can-apply(f;x), (L), weakPrecondSendR2{$a:ut2, $tg:ut2}(T; t; p; l; ds; P; f), isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), let x = a in b(x), locl_locl{locl_locl_compseq_tag_def:ObjectId}(b; a), f o' g, locl(a), (x,yL. P(x;y)) |
d1:(